COMMENT ⊗   VALID 00007 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	% boomac revised for clttex
C00003 00003	% bbnotation
C00006 00004	% formatting  internal and external definitions
C00008 00005	% boo versions of special font and formatting using active chars  |,/
C00011 00006	% other
C00012 00007	% setup magnification, page, font parameters
C00013 ENDMK
C⊗;
% boomac revised for clttex
%  
%  source on ESS,CLT
%  
%  see [TEX,CLT] for sources
%  
%  clttex.doc for documentation
%  cltfnt.tex
%  cltsty.tex
%  cltmac.tex


% bbnotation


\def\qNIL{{\tt NIL}}
\def\qT{{\tt T}}
\def\qF{{\tt F}}

\def\qtrue{{\bf true}}
\def\qfalse{{\bf false}}

\def\qat{\inmmode{\mathinner{\hbox{\bf at}}}}
\def\qa{\inmmode{\mathinner{\hbox{\bf a}}}}
\def\qaa{\inmmode{\mathinner{\hbox{\bf aa}}}}
\def\qd{\inmmode{\mathinner{\hbox{\bf d}}}}
\def\qda{\inmmode{\mathinner{\hbox{\bf da}}}}
\def\qdd{\inmmode{\mathinner{\hbox{\bf dd}}}}
\def\qad{\inmmode{\mathinner{\hbox{\bf ad}}}}
\def\qada{\inmmode{\mathinner{\hbox{\bf ada}}}}
\def\qadd{\inmmode{\mathinner{\hbox{\bf add}}}}
\def\qadda{\inmmode{\mathinner{\hbox{\bf adda}}}}
\def\qaddd{\inmmode{\mathinner{\hbox{\bf addd}}}}
\def\qn{\inmmode{\mathinner{\hbox{\bf n}}}}

\def\qeq{\inmmode{\mathrel{\hbox{\bf eq}}}}
\def\qcons{\inmmode{\mathrel{\raise .3ex\hbox{$\scriptscriptstyle{\bullet}$}}}}
\def\qapp{\inmmode{\mathrel{\ast}}}
\def\qlist#1{\inmmode{\mathopen{<} #1 \mathclose{>}}}

\def\qif{\inmmode{\mathinner{\hbox{\bf if}}\>}}
\def\qthen{\inmmode{\>\mathbin{\hbox{\bf then}}\>}}
\def\qelsif{\inmmode{\>\mathbin{\hbox{\bf else if}}\>}}
\def\qelseif{\inmmode{\>\mathbin{\hbox{\bf else if}}\>}}
\def\qelse{\inmmode{\>\mathinner{\hbox{\bf else}}\>}}
\def\qgo{\inmmode{\mathinner{\hbox{\bf go}}\>}}


\def\qequal{\inmmode{\mathrel{\dot{=}}}}
\def\qmem{\inmmode{\mathrel{\dot{\in}}}}

\def\qor{\inmmode{\mathrel{\dot{\vee}}}}
\def\qand{\inmmode{\mathrel{\dot{\wedge}}}}
\def\qnot{\inmmode{\mathinner{\dot{\lnot}}}}

\def\qlt{\inmmode{\mathrel{\dot{<}}}}
\def\qlte{\inmmode{\mathrel{\dot{\leq}}}}
\def\qgt{\inmmode{\mathrel{\dot{>}}}}
\def\qgte{\inmmode{\mathrel{\dot{\geq}}}}

\def\qp{\inmmode{\phi}}


\def\mkop#1{\inmmode{\mathinner{\hbox{\it #1}}}}

\def\div{\mathbin{\hbox{\rm\char`\/}}} % forslash


% formatting  internal and external definitions

\def\edefun#1#2{\hbox{!!?? External definition of /#1/ ??!!}}


\catcode`@=11 % borrow the private macros of PLAIN (with care)

%  \def\begindefun#1#2{%  for printing internal programs
%  \par
%  \noindent\llap{!!??}/#1/??!!
%  %  \vskip -\abovedisplayskip
%  $$\let\par=\endgraf \begingroup\smallsize \ttverbatim \parskip=\z@
%     \catcode`\|=0  \rightskip-5pc  \defunfinish}
%  
%  {\catcode`\|=0 |catcode`|\=\other % | is temporary escape character
%    |obeylines % end of line is active
%    |gdef|defunfinish#1↑↑M#2\enddefun{#1|vbox{#2}|endgroup|endgroup$$}}

\def\begindefun{\par\begingroup\parskip 0pt \figsize \tt\obeylines\obeyspaces
\everypar{\strut}}
\def\enddefun{\endgroup\par\noindent}

\catcode`@=12 % at signs are no longer letters


\def\beginlisp#1\endlisp{\relax}
% boo versions of special font and formatting using active chars  |,/
%  from manual.tex[tex,dek]

% quick and dirty mkop
\catcode`/=13 
\def/#1/{\inmmode{\mathinner{\hbox{\it #1}}}}


\def\|{\leavevmode\hbox{\tt\char`\|}} % vertical line

{\obeyspaces\gdef {\ }}


% macros for verbatim scanning
\chardef\other=12
%  \def\ttverbatim{\begingroup
%    \catcode`\\=\other
%    \catcode`\{=\other
%    \catcode`\}=\other
%    \catcode`\$=\other
%    \catcode`\&=\other
%    \catcode`\#=\other
%    \catcode`\%=\other
%    \catcode`\~=\other
%    \catcode`\/=\other
%    \catcode`\_=\other
%    \catcode`\↑=\other
%    \obeyspaces \obeylines \tt}

% macros for verbatim scanning
\def\ttverbatim{\begingroup
  \catcode`\\=\other
  \catcode`\{=\other
  \catcode`\}=\other
  \catcode`\$=\other
  \catcode`\&=\other
  \catcode`\#=\other
  \catcode`\%=\other
  \catcode`\~=\other
  \catcode`\/=\other
  \catcode`\_=\other
  \catcode`\↑=\other
%  \mathcode`\!="7021
\mathcode`\'="7027
\mathcode`\(="7028
\mathcode`\)="7029
\mathcode`\*="702A
%  \mathcode`\+="702B
%  \mathcode`\,="702C
\mathcode`\-="702D
\mathcode`\.="702E
\mathcode`\/="702F
\mathcode`\:="703A
%  \mathcode`\;="703B
\mathcode`\<="703C
\mathcode`\=="703D
\mathcode`\>="703E
\mathcode`\?="703F
%  \mathcode`\[="705B
\mathcode`\\="705C
%  \mathcode`\]="705D
\mathcode`\_="705F
%  \mathcode`\{="707B
%  \mathcode`\}="707D
  \obeyspaces\obeylines \tt}

\def\begintt{$$\let\par=\endgraf \ttverbatim \parskip=\z@
  \catcode`\|=0 \rightskip-5pc \ttfinish}
{\catcode`\|=0 |catcode`|\=\other % | is temporary escape character
  |obeylines % end of line is active
  |gdef|ttfinish#1↑↑M#2\endtt{#1|vbox{#2}|endgroup$$}}

\catcode`\|=\active
{\obeylines \gdef|{\ttverbatim \spaceskip\ttglue \let↑↑M=\  \let|=\endgroup}}


% other

\def\limp{\,\rightarrow\,}
\def\liff{\>\leftrightarrow\>}
\def\lor{\,\vee\,}
\def\land{\,\wedge\,}

\def\lisp{{\rm Lisp}}
\def\clisp{{\rm Common\ Lisp}}

% setup magnification, page, font parameters

%  \mag\magstephalf
\mag\magstep1
\hsize 6.0 true in
\vsize 8.25 true in 
\voffset=12pt
\hoffset= .5 true in
\hfuzz=5pt
\vfuzz=5pt

\topskip=\topskipdim
\parskip= 6pt plus 1pt % half normal baseline??

\parindent 20pt

% setup non-plain fonts
\def\normalsizehook{\rumnormalsizehook}
\let\figsizehook\rumfigsizehook
\let\fntsizehook\rumfntsizehook

\draftfootline{Programming and Proving}%
\draftheadline{{\tenbf \chapternum}}{{\tenbf \chaptername}}

\normalsize
\raggedbottom